Nuprl Lemma : ma-empty-compat-left
11,40
postcript
pdf
A
:MsgA. ||+
A
latex
Definitions
x
:
A
.
B
(
x
)
,
A
||+
B
,
P
&
Q
,
t
T
Lemmas
ma-empty-compatible-left
,
ma-empty-frame-compatible-left
,
msga
wf
origin
A:MsgA. ||+ A A:MsgA. ||+ A x:A. B(x)
T